\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $a$:ecl(${\it ds}$; ${\it da}$), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List). 
\\[0ex](ecl{-}trans{-}normal($v$)
\\[0ex]$\wedge$ ($\forall$$n$:$\mathbb{N}^{+}$. (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($n$,$L$)) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($v$))))
\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\wedge$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)($n$,${\it L'}$))))
\-\\[0ex]$\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($n$,$L$)))
\-\\[0ex]$\wedge$ ($\forall$$m$:$\mathbb{N}$. (ecl{-}act(${\it ds}$; ${\it da}$; $m$; $a$)($L$)) $\Leftarrow\!\Rightarrow$ (ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $v$)($m$,$L$))))
\\[0ex]$\Rightarrow$ (ecl{-}halt(${\it ds}$; ${\it da}$; $a$)(0,$L$))
\\[0ex]$\Rightarrow$ (\=ecl{-}trans{-}state(reset{-}ecl{-}tuple($v$); $L$)\+
\\[0ex]=
\\[0ex]ecl{-}trans{-}init(reset{-}ecl{-}tuple($v$))
\\[0ex]$\in$ ecl{-}trans{-}type(reset{-}ecl{-}tuple($v$)))
\-
\end{tabbing}